Left Termination proof of /tmp/tmpHUUzmJ/perm.pl

Left Termination of the query pattern perm1_in_2(g, g) w.r.t. the given Prolog program could successfully be proven:

↳ Prolog

  ↳ PrologToPiTRSProof

Clauses:

perm1(L, M) :- ','(eq_len1(L, M), same_sets(L, M)).
eq_len1([], []).
eq_len1(.(X, Xs), .(X1, Ys)) :- eq_len1(Xs, Ys).
member(X, .(X, X1)).
member(X, .(X1, T)) :- member(X, T).
same_sets([], X).
same_sets(.(X, Xs), L) :- ','(member(X, L), same_sets(Xs, L)).

Queries:

perm1(g,g).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
perm1_in: (b,b)
eq_len1_in: (b,b)
same_sets_in: (b,b)
member_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

perm1_in_gg(L, M) → U1_gg(L, M, eq_len1_in_gg(L, M))
eq_len1_in_gg([], []) → eq_len1_out_gg([], [])
eq_len1_in_gg(.(X, Xs), .(X1, Ys)) → U3_gg(X, Xs, X1, Ys, eq_len1_in_gg(Xs, Ys))
U3_gg(X, Xs, X1, Ys, eq_len1_out_gg(Xs, Ys)) → eq_len1_out_gg(.(X, Xs), .(X1, Ys))
U1_gg(L, M, eq_len1_out_gg(L, M)) → U2_gg(L, M, same_sets_in_gg(L, M))
same_sets_in_gg([], X) → same_sets_out_gg([], X)
same_sets_in_gg(.(X, Xs), L) → U5_gg(X, Xs, L, member_in_gg(X, L))
member_in_gg(X, .(X, X1)) → member_out_gg(X, .(X, X1))
member_in_gg(X, .(X1, T)) → U4_gg(X, X1, T, member_in_gg(X, T))
U4_gg(X, X1, T, member_out_gg(X, T)) → member_out_gg(X, .(X1, T))
U5_gg(X, Xs, L, member_out_gg(X, L)) → U6_gg(X, Xs, L, same_sets_in_gg(Xs, L))
U6_gg(X, Xs, L, same_sets_out_gg(Xs, L)) → same_sets_out_gg(.(X, Xs), L)
U2_gg(L, M, same_sets_out_gg(L, M)) → perm1_out_gg(L, M)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

perm1_in_gg(L, M) → U1_gg(L, M, eq_len1_in_gg(L, M))
eq_len1_in_gg([], []) → eq_len1_out_gg([], [])
eq_len1_in_gg(.(X, Xs), .(X1, Ys)) → U3_gg(X, Xs, X1, Ys, eq_len1_in_gg(Xs, Ys))
U3_gg(X, Xs, X1, Ys, eq_len1_out_gg(Xs, Ys)) → eq_len1_out_gg(.(X, Xs), .(X1, Ys))
U1_gg(L, M, eq_len1_out_gg(L, M)) → U2_gg(L, M, same_sets_in_gg(L, M))
same_sets_in_gg([], X) → same_sets_out_gg([], X)
same_sets_in_gg(.(X, Xs), L) → U5_gg(X, Xs, L, member_in_gg(X, L))
member_in_gg(X, .(X, X1)) → member_out_gg(X, .(X, X1))
member_in_gg(X, .(X1, T)) → U4_gg(X, X1, T, member_in_gg(X, T))
U4_gg(X, X1, T, member_out_gg(X, T)) → member_out_gg(X, .(X1, T))
U5_gg(X, Xs, L, member_out_gg(X, L)) → U6_gg(X, Xs, L, same_sets_in_gg(Xs, L))
U6_gg(X, Xs, L, same_sets_out_gg(Xs, L)) → same_sets_out_gg(.(X, Xs), L)
U2_gg(L, M, same_sets_out_gg(L, M)) → perm1_out_gg(L, M)

PERM1_IN_GG(L, M) → U1_GG(L, M, eq_len1_in_gg(L, M))
PERM1_IN_GG(L, M) → EQ_LEN1_IN_GG(L, M)
EQ_LEN1_IN_GG(.(X, Xs), .(X1, Ys)) → U3_GG(X, Xs, X1, Ys, eq_len1_in_gg(Xs, Ys))
EQ_LEN1_IN_GG(.(X, Xs), .(X1, Ys)) → EQ_LEN1_IN_GG(Xs, Ys)
U1_GG(L, M, eq_len1_out_gg(L, M)) → U2_GG(L, M, same_sets_in_gg(L, M))
U1_GG(L, M, eq_len1_out_gg(L, M)) → SAME_SETS_IN_GG(L, M)
SAME_SETS_IN_GG(.(X, Xs), L) → U5_GG(X, Xs, L, member_in_gg(X, L))
SAME_SETS_IN_GG(.(X, Xs), L) → MEMBER_IN_GG(X, L)
MEMBER_IN_GG(X, .(X1, T)) → U4_GG(X, X1, T, member_in_gg(X, T))
MEMBER_IN_GG(X, .(X1, T)) → MEMBER_IN_GG(X, T)
U5_GG(X, Xs, L, member_out_gg(X, L)) → U6_GG(X, Xs, L, same_sets_in_gg(Xs, L))
U5_GG(X, Xs, L, member_out_gg(X, L)) → SAME_SETS_IN_GG(Xs, L)

The TRS R consists of the following rules:

perm1_in_gg(L, M) → U1_gg(L, M, eq_len1_in_gg(L, M))
eq_len1_in_gg([], []) → eq_len1_out_gg([], [])
eq_len1_in_gg(.(X, Xs), .(X1, Ys)) → U3_gg(X, Xs, X1, Ys, eq_len1_in_gg(Xs, Ys))
U3_gg(X, Xs, X1, Ys, eq_len1_out_gg(Xs, Ys)) → eq_len1_out_gg(.(X, Xs), .(X1, Ys))
U1_gg(L, M, eq_len1_out_gg(L, M)) → U2_gg(L, M, same_sets_in_gg(L, M))
same_sets_in_gg([], X) → same_sets_out_gg([], X)
same_sets_in_gg(.(X, Xs), L) → U5_gg(X, Xs, L, member_in_gg(X, L))
member_in_gg(X, .(X, X1)) → member_out_gg(X, .(X, X1))
member_in_gg(X, .(X1, T)) → U4_gg(X, X1, T, member_in_gg(X, T))
U4_gg(X, X1, T, member_out_gg(X, T)) → member_out_gg(X, .(X1, T))
U5_gg(X, Xs, L, member_out_gg(X, L)) → U6_gg(X, Xs, L, same_sets_in_gg(Xs, L))
U6_gg(X, Xs, L, same_sets_out_gg(Xs, L)) → same_sets_out_gg(.(X, Xs), L)
U2_gg(L, M, same_sets_out_gg(L, M)) → perm1_out_gg(L, M)

The argument filtering Pi contains the following mapping:
perm1_in_gg(x1, x2) = perm1_in_gg(x1, x2)
U1_gg(x1, x2, x3) = U1_gg(x1, x2, x3)
eq_len1_in_gg(x1, x2) = eq_len1_in_gg(x1, x2)
[] = []
eq_len1_out_gg(x1, x2) = eq_len1_out_gg
.(x1, x2) = .(x1, x2)
U3_gg(x1, x2, x3, x4, x5) = U3_gg(x5)
U2_gg(x1, x2, x3) = U2_gg(x3)
same_sets_in_gg(x1, x2) = same_sets_in_gg(x1, x2)
same_sets_out_gg(x1, x2) = same_sets_out_gg
U5_gg(x1, x2, x3, x4) = U5_gg(x2, x3, x4)
member_in_gg(x1, x2) = member_in_gg(x1, x2)
member_out_gg(x1, x2) = member_out_gg
U4_gg(x1, x2, x3, x4) = U4_gg(x4)
U6_gg(x1, x2, x3, x4) = U6_gg(x4)
perm1_out_gg(x1, x2) = perm1_out_gg
U5_GG(x1, x2, x3, x4) = U5_GG(x2, x3, x4)
U6_GG(x1, x2, x3, x4) = U6_GG(x4)
MEMBER_IN_GG(x1, x2) = MEMBER_IN_GG(x1, x2)
U1_GG(x1, x2, x3) = U1_GG(x1, x2, x3)
PERM1_IN_GG(x1, x2) = PERM1_IN_GG(x1, x2)
U4_GG(x1, x2, x3, x4) = U4_GG(x4)
U2_GG(x1, x2, x3) = U2_GG(x3)
U3_GG(x1, x2, x3, x4, x5) = U3_GG(x5)
SAME_SETS_IN_GG(x1, x2) = SAME_SETS_IN_GG(x1, x2)
EQ_LEN1_IN_GG(x1, x2) = EQ_LEN1_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

PERM1_IN_GG(L, M) → U1_GG(L, M, eq_len1_in_gg(L, M))
PERM1_IN_GG(L, M) → EQ_LEN1_IN_GG(L, M)
EQ_LEN1_IN_GG(.(X, Xs), .(X1, Ys)) → U3_GG(X, Xs, X1, Ys, eq_len1_in_gg(Xs, Ys))
EQ_LEN1_IN_GG(.(X, Xs), .(X1, Ys)) → EQ_LEN1_IN_GG(Xs, Ys)
U1_GG(L, M, eq_len1_out_gg(L, M)) → U2_GG(L, M, same_sets_in_gg(L, M))
U1_GG(L, M, eq_len1_out_gg(L, M)) → SAME_SETS_IN_GG(L, M)
SAME_SETS_IN_GG(.(X, Xs), L) → U5_GG(X, Xs, L, member_in_gg(X, L))
SAME_SETS_IN_GG(.(X, Xs), L) → MEMBER_IN_GG(X, L)
MEMBER_IN_GG(X, .(X1, T)) → U4_GG(X, X1, T, member_in_gg(X, T))
MEMBER_IN_GG(X, .(X1, T)) → MEMBER_IN_GG(X, T)
U5_GG(X, Xs, L, member_out_gg(X, L)) → U6_GG(X, Xs, L, same_sets_in_gg(Xs, L))
U5_GG(X, Xs, L, member_out_gg(X, L)) → SAME_SETS_IN_GG(Xs, L)

The TRS R consists of the following rules:

perm1_in_gg(L, M) → U1_gg(L, M, eq_len1_in_gg(L, M))
eq_len1_in_gg([], []) → eq_len1_out_gg([], [])
eq_len1_in_gg(.(X, Xs), .(X1, Ys)) → U3_gg(X, Xs, X1, Ys, eq_len1_in_gg(Xs, Ys))
U3_gg(X, Xs, X1, Ys, eq_len1_out_gg(Xs, Ys)) → eq_len1_out_gg(.(X, Xs), .(X1, Ys))
U1_gg(L, M, eq_len1_out_gg(L, M)) → U2_gg(L, M, same_sets_in_gg(L, M))
same_sets_in_gg([], X) → same_sets_out_gg([], X)
same_sets_in_gg(.(X, Xs), L) → U5_gg(X, Xs, L, member_in_gg(X, L))
member_in_gg(X, .(X, X1)) → member_out_gg(X, .(X, X1))
member_in_gg(X, .(X1, T)) → U4_gg(X, X1, T, member_in_gg(X, T))
U4_gg(X, X1, T, member_out_gg(X, T)) → member_out_gg(X, .(X1, T))
U5_gg(X, Xs, L, member_out_gg(X, L)) → U6_gg(X, Xs, L, same_sets_in_gg(Xs, L))
U6_gg(X, Xs, L, same_sets_out_gg(Xs, L)) → same_sets_out_gg(.(X, Xs), L)
U2_gg(L, M, same_sets_out_gg(L, M)) → perm1_out_gg(L, M)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN_GG(X, .(X1, T)) → MEMBER_IN_GG(X, T)

The TRS R consists of the following rules:

perm1_in_gg(L, M) → U1_gg(L, M, eq_len1_in_gg(L, M))
eq_len1_in_gg([], []) → eq_len1_out_gg([], [])
eq_len1_in_gg(.(X, Xs), .(X1, Ys)) → U3_gg(X, Xs, X1, Ys, eq_len1_in_gg(Xs, Ys))
U3_gg(X, Xs, X1, Ys, eq_len1_out_gg(Xs, Ys)) → eq_len1_out_gg(.(X, Xs), .(X1, Ys))
U1_gg(L, M, eq_len1_out_gg(L, M)) → U2_gg(L, M, same_sets_in_gg(L, M))
same_sets_in_gg([], X) → same_sets_out_gg([], X)
same_sets_in_gg(.(X, Xs), L) → U5_gg(X, Xs, L, member_in_gg(X, L))
member_in_gg(X, .(X, X1)) → member_out_gg(X, .(X, X1))
member_in_gg(X, .(X1, T)) → U4_gg(X, X1, T, member_in_gg(X, T))
U4_gg(X, X1, T, member_out_gg(X, T)) → member_out_gg(X, .(X1, T))
U5_gg(X, Xs, L, member_out_gg(X, L)) → U6_gg(X, Xs, L, same_sets_in_gg(Xs, L))
U6_gg(X, Xs, L, same_sets_out_gg(Xs, L)) → same_sets_out_gg(.(X, Xs), L)
U2_gg(L, M, same_sets_out_gg(L, M)) → perm1_out_gg(L, M)

The argument filtering Pi contains the following mapping:
perm1_in_gg(x1, x2) = perm1_in_gg(x1, x2)
U1_gg(x1, x2, x3) = U1_gg(x1, x2, x3)
eq_len1_in_gg(x1, x2) = eq_len1_in_gg(x1, x2)
[] = []
eq_len1_out_gg(x1, x2) = eq_len1_out_gg
.(x1, x2) = .(x1, x2)
U3_gg(x1, x2, x3, x4, x5) = U3_gg(x5)
U2_gg(x1, x2, x3) = U2_gg(x3)
same_sets_in_gg(x1, x2) = same_sets_in_gg(x1, x2)
same_sets_out_gg(x1, x2) = same_sets_out_gg
U5_gg(x1, x2, x3, x4) = U5_gg(x2, x3, x4)
member_in_gg(x1, x2) = member_in_gg(x1, x2)
member_out_gg(x1, x2) = member_out_gg
U4_gg(x1, x2, x3, x4) = U4_gg(x4)
U6_gg(x1, x2, x3, x4) = U6_gg(x4)
perm1_out_gg(x1, x2) = perm1_out_gg
MEMBER_IN_GG(x1, x2) = MEMBER_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN_GG(X, .(X1, T)) → MEMBER_IN_GG(X, T)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MEMBER_IN_GG(X, .(X1, T)) → MEMBER_IN_GG(X, T)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

MEMBER_IN_GG(X, .(X1, T)) → MEMBER_IN_GG(X, T)
The graph contains the following edges 1 >= 1, 2 > 2

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SAME_SETS_IN_GG(.(X, Xs), L) → U5_GG(X, Xs, L, member_in_gg(X, L))
U5_GG(X, Xs, L, member_out_gg(X, L)) → SAME_SETS_IN_GG(Xs, L)

The TRS R consists of the following rules:

perm1_in_gg(L, M) → U1_gg(L, M, eq_len1_in_gg(L, M))
eq_len1_in_gg([], []) → eq_len1_out_gg([], [])
eq_len1_in_gg(.(X, Xs), .(X1, Ys)) → U3_gg(X, Xs, X1, Ys, eq_len1_in_gg(Xs, Ys))
U3_gg(X, Xs, X1, Ys, eq_len1_out_gg(Xs, Ys)) → eq_len1_out_gg(.(X, Xs), .(X1, Ys))
U1_gg(L, M, eq_len1_out_gg(L, M)) → U2_gg(L, M, same_sets_in_gg(L, M))
same_sets_in_gg([], X) → same_sets_out_gg([], X)
same_sets_in_gg(.(X, Xs), L) → U5_gg(X, Xs, L, member_in_gg(X, L))
member_in_gg(X, .(X, X1)) → member_out_gg(X, .(X, X1))
member_in_gg(X, .(X1, T)) → U4_gg(X, X1, T, member_in_gg(X, T))
U4_gg(X, X1, T, member_out_gg(X, T)) → member_out_gg(X, .(X1, T))
U5_gg(X, Xs, L, member_out_gg(X, L)) → U6_gg(X, Xs, L, same_sets_in_gg(Xs, L))
U6_gg(X, Xs, L, same_sets_out_gg(Xs, L)) → same_sets_out_gg(.(X, Xs), L)
U2_gg(L, M, same_sets_out_gg(L, M)) → perm1_out_gg(L, M)

The argument filtering Pi contains the following mapping:
perm1_in_gg(x1, x2) = perm1_in_gg(x1, x2)
U1_gg(x1, x2, x3) = U1_gg(x1, x2, x3)
eq_len1_in_gg(x1, x2) = eq_len1_in_gg(x1, x2)
[] = []
eq_len1_out_gg(x1, x2) = eq_len1_out_gg
.(x1, x2) = .(x1, x2)
U3_gg(x1, x2, x3, x4, x5) = U3_gg(x5)
U2_gg(x1, x2, x3) = U2_gg(x3)
same_sets_in_gg(x1, x2) = same_sets_in_gg(x1, x2)
same_sets_out_gg(x1, x2) = same_sets_out_gg
U5_gg(x1, x2, x3, x4) = U5_gg(x2, x3, x4)
member_in_gg(x1, x2) = member_in_gg(x1, x2)
member_out_gg(x1, x2) = member_out_gg
U4_gg(x1, x2, x3, x4) = U4_gg(x4)
U6_gg(x1, x2, x3, x4) = U6_gg(x4)
perm1_out_gg(x1, x2) = perm1_out_gg
U5_GG(x1, x2, x3, x4) = U5_GG(x2, x3, x4)
SAME_SETS_IN_GG(x1, x2) = SAME_SETS_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SAME_SETS_IN_GG(.(X, Xs), L) → U5_GG(X, Xs, L, member_in_gg(X, L))
U5_GG(X, Xs, L, member_out_gg(X, L)) → SAME_SETS_IN_GG(Xs, L)

The TRS R consists of the following rules:

member_in_gg(X, .(X, X1)) → member_out_gg(X, .(X, X1))
member_in_gg(X, .(X1, T)) → U4_gg(X, X1, T, member_in_gg(X, T))
U4_gg(X, X1, T, member_out_gg(X, T)) → member_out_gg(X, .(X1, T))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
member_in_gg(x1, x2) = member_in_gg(x1, x2)
member_out_gg(x1, x2) = member_out_gg
U4_gg(x1, x2, x3, x4) = U4_gg(x4)
U5_GG(x1, x2, x3, x4) = U5_GG(x2, x3, x4)
SAME_SETS_IN_GG(x1, x2) = SAME_SETS_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

SAME_SETS_IN_GG(.(X, Xs), L) → U5_GG(Xs, L, member_in_gg(X, L))
U5_GG(Xs, L, member_out_gg) → SAME_SETS_IN_GG(Xs, L)

The TRS R consists of the following rules:

member_in_gg(X, .(X, X1)) → member_out_gg
member_in_gg(X, .(X1, T)) → U4_gg(member_in_gg(X, T))
U4_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

member_in_gg(x0, x1)
U4_gg(x0)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

U5_GG(Xs, L, member_out_gg) → SAME_SETS_IN_GG(Xs, L)
The graph contains the following edges 1 >= 1, 2 >= 2
SAME_SETS_IN_GG(.(X, Xs), L) → U5_GG(Xs, L, member_in_gg(X, L))
The graph contains the following edges 1 > 1, 2 >= 2

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

EQ_LEN1_IN_GG(.(X, Xs), .(X1, Ys)) → EQ_LEN1_IN_GG(Xs, Ys)

The TRS R consists of the following rules:

perm1_in_gg(L, M) → U1_gg(L, M, eq_len1_in_gg(L, M))
eq_len1_in_gg([], []) → eq_len1_out_gg([], [])
eq_len1_in_gg(.(X, Xs), .(X1, Ys)) → U3_gg(X, Xs, X1, Ys, eq_len1_in_gg(Xs, Ys))
U3_gg(X, Xs, X1, Ys, eq_len1_out_gg(Xs, Ys)) → eq_len1_out_gg(.(X, Xs), .(X1, Ys))
U1_gg(L, M, eq_len1_out_gg(L, M)) → U2_gg(L, M, same_sets_in_gg(L, M))
same_sets_in_gg([], X) → same_sets_out_gg([], X)
same_sets_in_gg(.(X, Xs), L) → U5_gg(X, Xs, L, member_in_gg(X, L))
member_in_gg(X, .(X, X1)) → member_out_gg(X, .(X, X1))
member_in_gg(X, .(X1, T)) → U4_gg(X, X1, T, member_in_gg(X, T))
U4_gg(X, X1, T, member_out_gg(X, T)) → member_out_gg(X, .(X1, T))
U5_gg(X, Xs, L, member_out_gg(X, L)) → U6_gg(X, Xs, L, same_sets_in_gg(Xs, L))
U6_gg(X, Xs, L, same_sets_out_gg(Xs, L)) → same_sets_out_gg(.(X, Xs), L)
U2_gg(L, M, same_sets_out_gg(L, M)) → perm1_out_gg(L, M)

The argument filtering Pi contains the following mapping:
perm1_in_gg(x1, x2) = perm1_in_gg(x1, x2)
U1_gg(x1, x2, x3) = U1_gg(x1, x2, x3)
eq_len1_in_gg(x1, x2) = eq_len1_in_gg(x1, x2)
[] = []
eq_len1_out_gg(x1, x2) = eq_len1_out_gg
.(x1, x2) = .(x1, x2)
U3_gg(x1, x2, x3, x4, x5) = U3_gg(x5)
U2_gg(x1, x2, x3) = U2_gg(x3)
same_sets_in_gg(x1, x2) = same_sets_in_gg(x1, x2)
same_sets_out_gg(x1, x2) = same_sets_out_gg
U5_gg(x1, x2, x3, x4) = U5_gg(x2, x3, x4)
member_in_gg(x1, x2) = member_in_gg(x1, x2)
member_out_gg(x1, x2) = member_out_gg
U4_gg(x1, x2, x3, x4) = U4_gg(x4)
U6_gg(x1, x2, x3, x4) = U6_gg(x4)
perm1_out_gg(x1, x2) = perm1_out_gg
EQ_LEN1_IN_GG(x1, x2) = EQ_LEN1_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

EQ_LEN1_IN_GG(.(X, Xs), .(X1, Ys)) → EQ_LEN1_IN_GG(Xs, Ys)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

EQ_LEN1_IN_GG(.(X, Xs), .(X1, Ys)) → EQ_LEN1_IN_GG(Xs, Ys)

From the DPs we obtained the following set of size-change graphs:

EQ_LEN1_IN_GG(.(X, Xs), .(X1, Ys)) → EQ_LEN1_IN_GG(Xs, Ys)
The graph contains the following edges 1 > 1, 2 > 2